(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 7))
(declare-fun v1 () (_ BitVec 7))
(declare-fun v2 () (_ BitVec 2))
(declare-fun v3 () (_ BitVec 7))
(declare-fun v4 () (_ BitVec 1))
(assert (let ((e5(_ bv7 5)))
(let ((e6 (ite (= v3 ((_ sign_extend 6) v4)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (ite (distinct v1 v0) (_ bv1 1) (_ bv0 1))))
(let ((e8 (ite (distinct ((_ zero_extend 6) v4) v1) (_ bv1 1) (_ bv0 1))))
(let ((e9 ((_ extract 0 0) e6)))
(let ((e10 (ite (distinct ((_ zero_extend 1) e6) v2) (_ bv1 1) (_ bv0 1))))
(let ((e11 ((_ sign_extend 1) e5)))
(let ((e12 (= v3 v3)))
(let ((e13 (distinct ((_ sign_extend 6) e8) v0)))
(let ((e14 (distinct v1 ((_ sign_extend 6) e8))))
(let ((e15 (distinct e11 ((_ sign_extend 4) v2))))
(let ((e16 (distinct e7 v4)))
(let ((e17 (distinct v2 ((_ sign_extend 1) e10))))
(let ((e18 (distinct ((_ sign_extend 6) e10) v1)))
(let ((e19 (distinct v4 e9)))
(let ((e20 (= ((_ sign_extend 6) e9) v3)))
(let ((e21 (= v0 ((_ zero_extend 6) e7))))
(let ((e22 (distinct v3 v0)))
(let ((e23 (distinct e9 e10)))
(let ((e24 (= ((_ zero_extend 6) e8) v0)))
(let ((e25 (= ((_ sign_extend 6) e10) v1)))
(let ((e26 (distinct ((_ zero_extend 5) v2) v1)))
(let ((e27 (distinct ((_ sign_extend 6) v4) v3)))
(let ((e28 (= ((_ sign_extend 6) e10) v1)))
(let ((e29 (= v0 ((_ sign_extend 6) e6))))
(let ((e30 (= e10 e8)))
(let ((e31 (= ((_ zero_extend 4) e9) e5)))
(let ((e32 (ite e13 e18 e28)))
(let ((e33 (or e14 e24)))
(let ((e34 (or e25 e21)))
(let ((e35 (ite e19 e15 e33)))
(let ((e36 (and e35 e23)))
(let ((e37 (= e36 e31)))
(let ((e38 (=> e34 e22)))
(let ((e39 (= e29 e29)))
(let ((e40 (and e32 e30)))
(let ((e41 (not e40)))
(let ((e42 (ite e41 e27 e39)))
(let ((e43 (and e42 e17)))
(let ((e44 (or e16 e38)))
(let ((e45 (ite e43 e37 e37)))
(let ((e46 (and e20 e45)))
(let ((e47 (ite e12 e46 e12)))
(let ((e48 (or e44 e26)))
(let ((e49 (and e48 e47)))
e49
))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
